\begin{tabbing}
$\forall$${\it es}$:ES, $l$:IdLnk, ${\it tg}$:Id, $A$:Type.
\\[0ex]($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (valtype($e$) $\subseteq$r $A$))
\\[0ex]$\Rightarrow$ (\=es{-}in{-}port(${\it es}$;$l$;${\it tg}$)\+
\\[0ex]=
\\[0ex]es{-}triggers(${\it es}$;destination($l$);$\otimes$;es{-}in{-}port{-}conds($A$;$l$;${\it tg}$))
\\[0ex]$\in$ AbsInterface($A$))
\-
\end{tabbing}